YES 1.449 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  (((==) :: Eq a => [a ->  [a ->  Bool) :: Eq a => [a ->  [a ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  (((==) :: Eq a => [a ->  [a ->  Bool) :: Eq a => [a ->  [a ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  ((==) :: Eq a => [a ->  [a ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv1100), Succ(xv401000)) → new_primPlusNat(xv1100, xv401000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30100), Succ(xv40100)) → new_primMulNat(xv30100, Succ(xv40100))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv4000)) → new_primEqNat(xv3000, xv4000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_@2, bcg), bch)), hg), bbb)) → new_esEs2(xv300, xv400, bcg, bch)
new_esEs1(Right(xv300), Right(xv400), df, app(ty_Maybe, dg)) → new_esEs0(xv300, xv400, dg)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), hg), app(app(ty_@2, bad), bae))) → new_esEs2(xv302, xv402, bad, bae)
new_esEs(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, df), app(ty_[], eb))) → new_esEs(xv300, xv400, eb)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), app(ty_Maybe, bba)), bbb)) → new_esEs0(xv301, xv401, bba)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, app(ty_Maybe, bba), bbb) → new_esEs0(xv301, xv401, bba)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(ty_[], gh)), ge)) → new_esEs(xv300, xv400, gh)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(app(ty_@3, hc), hd), he)), ge)) → new_esEs3(xv300, xv400, hc, hd, he)
new_esEs(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, df), app(app(ty_@2, ec), ed))) → new_esEs2(xv300, xv400, ec, ed)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, hg, app(ty_Maybe, hh)) → new_esEs0(xv302, xv402, hh)
new_esEs0(Just(xv300), Just(xv400), app(ty_Maybe, bb)) → new_esEs0(xv300, xv400, bb)
new_esEs0(Just(xv300), Just(xv400), app(ty_[], be)) → new_esEs(xv300, xv400, be)
new_esEs1(Left(xv300), Left(xv400), app(app(ty_Either, ce), cf), cd) → new_esEs1(xv300, xv400, ce, cf)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_Maybe, bcc)), hg), bbb)) → new_esEs0(xv300, xv400, bcc)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fa, app(app(app(ty_@3, ga), gb), gc)) → new_esEs3(xv301, xv401, ga, gb, gc)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, app(ty_[], bbe), bbb) → new_esEs(xv301, xv401, bbe)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, fa), app(ty_[], ff))) → new_esEs(xv301, xv401, ff)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_Either, bcd), bce), hg, bbb) → new_esEs1(xv300, xv400, bcd, bce)
new_esEs1(Left(xv300), Left(xv400), app(app(ty_@2, da), db), cd) → new_esEs2(xv300, xv400, da, db)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(app(ty_@3, bda), bdb), bdc)), hg), bbb)) → new_esEs3(xv300, xv400, bda, bdb, bdc)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(ty_Maybe, gd), ge) → new_esEs0(xv300, xv400, gd)
new_esEs(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(ty_[], cg)), cd)) → new_esEs(xv300, xv400, cg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, app(app(ty_Either, bbc), bbd), bbb) → new_esEs1(xv301, xv401, bbc, bbd)
new_esEs0(Just(xv300), Just(xv400), app(app(app(ty_@3, bh), ca), cb)) → new_esEs3(xv300, xv400, bh, ca, cb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(ty_@2, bcg), bch), hg, bbb) → new_esEs2(xv300, xv400, bcg, bch)
new_esEs(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(app(ty_@3, dc), dd), de)), cd)) → new_esEs3(xv300, xv400, dc, dd, de)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, fa), app(app(ty_Either, fc), fd))) → new_esEs1(xv301, xv401, fc, fd)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), hg), app(ty_Maybe, hh))) → new_esEs0(xv302, xv402, hh)
new_esEs(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(ty_@2, da), db)), cd)) → new_esEs2(xv300, xv400, da, db)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(ty_Either, gf), gg)), ge)) → new_esEs1(xv300, xv400, gf, gg)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_Maybe, bcc), hg, bbb) → new_esEs0(xv300, xv400, bcc)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), app(app(app(ty_@3, bbh), bca), bcb)), bbb)) → new_esEs3(xv301, xv401, bbh, bca, bcb)
new_esEs1(Right(xv300), Right(xv400), df, app(ty_[], eb)) → new_esEs(xv300, xv400, eb)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_Either, gf), gg), ge) → new_esEs1(xv300, xv400, gf, gg)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), hg), app(ty_[], bac))) → new_esEs(xv302, xv402, bac)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(app(app(ty_@3, hc), hd), he), ge) → new_esEs3(xv300, xv400, hc, hd, he)
new_esEs(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, df), app(ty_Maybe, dg))) → new_esEs0(xv300, xv400, dg)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), app(ty_[], bbe)), bbb)) → new_esEs(xv301, xv401, bbe)
new_esEs(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(app(ty_Either, ce), cf)), cd)) → new_esEs1(xv300, xv400, ce, cf)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), app(app(ty_@2, bbf), bbg)), bbb)) → new_esEs2(xv301, xv401, bbf, bbg)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, fa), app(app(ty_@2, fg), fh))) → new_esEs2(xv301, xv401, fg, fh)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, hg, app(app(app(ty_@3, baf), bag), bah)) → new_esEs3(xv302, xv402, baf, bag, bah)
new_esEs(:(Left(xv300), xv31), :(Left(xv400), xv41), app(app(ty_Either, app(ty_Maybe, cc)), cd)) → new_esEs0(xv300, xv400, cc)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(ty_[], bcf)), hg), bbb)) → new_esEs(xv300, xv400, bcf)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, hg, app(ty_[], bac)) → new_esEs(xv302, xv402, bac)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fa, app(app(ty_@2, fg), fh)) → new_esEs2(xv301, xv401, fg, fh)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, app(app(ty_Either, bcd), bce)), hg), bbb)) → new_esEs1(xv300, xv400, bcd, bce)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fa, app(ty_Maybe, fb)) → new_esEs0(xv301, xv401, fb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(ty_[], bcf), hg, bbb) → new_esEs(xv300, xv400, bcf)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(app(ty_@2, ha), hb), ge) → new_esEs2(xv300, xv400, ha, hb)
new_esEs(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(ty_[], be))) → new_esEs(xv300, xv400, be)
new_esEs1(Right(xv300), Right(xv400), df, app(app(ty_Either, dh), ea)) → new_esEs1(xv300, xv400, dh, ea)
new_esEs1(Left(xv300), Left(xv400), app(ty_Maybe, cc), cd) → new_esEs0(xv300, xv400, cc)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), hg), app(app(app(ty_@3, baf), bag), bah))) → new_esEs3(xv302, xv402, baf, bag, bah)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fa, app(app(ty_Either, fc), fd)) → new_esEs1(xv301, xv401, fc, fd)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, app(app(app(ty_@3, bbh), bca), bcb), bbb) → new_esEs3(xv301, xv401, bbh, bca, bcb)
new_esEs0(Just(xv300), Just(xv400), app(app(ty_@2, bf), bg)) → new_esEs2(xv300, xv400, bf, bg)
new_esEs(:(xv30, xv31), :(xv40, xv41), ba) → new_esEs(xv31, xv41, ba)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), fa, app(ty_[], ff)) → new_esEs(xv301, xv401, ff)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, hg, app(app(ty_@2, bad), bae)) → new_esEs2(xv302, xv402, bad, bae)
new_esEs0(Just(xv300), Just(xv400), app(app(ty_Either, bc), bd)) → new_esEs1(xv300, xv400, bc, bd)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), hg), app(app(ty_Either, baa), bab))) → new_esEs1(xv302, xv402, baa, bab)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, app(app(ty_@2, bbf), bbg), bbb) → new_esEs2(xv301, xv401, bbf, bbg)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(ty_Maybe, gd)), ge)) → new_esEs0(xv300, xv400, gd)
new_esEs1(Right(xv300), Right(xv400), df, app(app(app(ty_@3, ee), ef), eg)) → new_esEs3(xv300, xv400, ee, ef, eg)
new_esEs(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(ty_@2, bf), bg))) → new_esEs2(xv300, xv400, bf, bg)
new_esEs(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(ty_Maybe, bb))) → new_esEs0(xv300, xv400, bb)
new_esEs(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(app(ty_@3, bh), ca), cb))) → new_esEs3(xv300, xv400, bh, ca, cb)
new_esEs1(Right(xv300), Right(xv400), df, app(app(ty_@2, ec), ed)) → new_esEs2(xv300, xv400, ec, ed)
new_esEs(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, df), app(app(app(ty_@3, ee), ef), eg))) → new_esEs3(xv300, xv400, ee, ef, eg)
new_esEs(:(Just(xv300), xv31), :(Just(xv400), xv41), app(ty_Maybe, app(app(ty_Either, bc), bd))) → new_esEs1(xv300, xv400, bc, bd)
new_esEs2(@2(xv300, xv301), @2(xv400, xv401), app(ty_[], gh), ge) → new_esEs(xv300, xv400, gh)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, app(app(ty_@2, ha), hb)), ge)) → new_esEs2(xv300, xv400, ha, hb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), hf, hg, app(app(ty_Either, baa), bab)) → new_esEs1(xv302, xv402, baa, bab)
new_esEs(:(Right(xv300), xv31), :(Right(xv400), xv41), app(app(ty_Either, df), app(app(ty_Either, dh), ea))) → new_esEs1(xv300, xv400, dh, ea)
new_esEs1(Left(xv300), Left(xv400), app(ty_[], cg), cd) → new_esEs(xv300, xv400, cg)
new_esEs(:(@3(xv300, xv301, xv302), xv31), :(@3(xv400, xv401, xv402), xv41), app(app(app(ty_@3, hf), app(app(ty_Either, bbc), bbd)), bbb)) → new_esEs1(xv301, xv401, bbc, bbd)
new_esEs1(Left(xv300), Left(xv400), app(app(app(ty_@3, dc), dd), de), cd) → new_esEs3(xv300, xv400, dc, dd, de)
new_esEs(:(xv30, xv31), :(xv40, xv41), app(ty_[], eh)) → new_esEs(xv30, xv40, eh)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, fa), app(ty_Maybe, fb))) → new_esEs0(xv301, xv401, fb)
new_esEs3(@3(xv300, xv301, xv302), @3(xv400, xv401, xv402), app(app(app(ty_@3, bda), bdb), bdc), hg, bbb) → new_esEs3(xv300, xv400, bda, bdb, bdc)
new_esEs(:(@2(xv300, xv301), xv31), :(@2(xv400, xv401), xv41), app(app(ty_@2, fa), app(app(app(ty_@3, ga), gb), gc))) → new_esEs3(xv301, xv401, ga, gb, gc)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: